Edinburgh LCF: A Mechanized Logic of Computation